Issue4121-1.agda:15,5-7
Not in scope:
  c′ at Issue4121-1.agda:15,5-7
when scope checking c′
